ds:(IdType), da:(IdKndType), A:Type, X:Interface(ds;da;Top + A), es:ES.
es-decl(es;ds;da)  ([[interface-right(X)]] = es-interface-right([[X]])  AbsInterface(A)) 

latex

Definitions

es-decl(es;ds;da), ES, Interface(ds;da;A), Knd, Id, Type, <a, b>, f(a), interface-right(X), s = t, x:AB(x), E, AbsInterface(A), es-interface-right(X), t  T, [[X]], left + right, Top, x:A. B(x), P  Q, s ~ t, in-interface(es;X;e), f o g  , can-apply(f;x), do-apply(f;x), fpf dom compose compseq tag def, P  Q, P & Q, , if b then t else f fi , fpf ap compose compseq tag def, interface-val(es;X;e), invert-union(x), ff, A, False, t.1, b, x:A  B(x), a:A fp B(a), inr x , , Unit, x:A.B(x), Void

Lemmas

it wf, invert-union wf, assert of bnot, eqff to assert, iff transitivity, eqtt to assert, abs-interface wf, es-interface-right wf, interface-right wf, es-E wf, Id wf, Knd wf, top wf, interface wf, event system wf, es-decl wf